formalmethodswikiaorg-20200214-history
ProCoS-WG
---- The final report (10 pages) is available in format: [ftp://ftp.cs.reading.ac.uk/pub/formal/jpb/procos-wg.ps A ProCoS-WG Working Group Project Final Report:ESPRIT Working Group 8694], Jonathan Bowen (The University of Reading, UK), (Oxford University, UK), Hans Langmaack (Christian-Albrechts-Universität zu Kiel, Germany), Ernst-Rüdiger Olderog (Universität Oldenburg, Germany) and Anders P. Ravn (Technical University of Denmark), [http://www.wi.leidenuniv.nl/~beatcs/ Bulletin of the European Association for Theoretical Computer Science] (EATCS), [http://www.wi.leidenuniv.nl/~beatcs/toc/beatcs64.txt Volume 64], pages 63–72, February 1998. The last major meeting was held 7–9 April 1997, at the , UK, in conjunction with ZUM'97. A Hardware Synthesis and Verification Workshop was held at Cornell University, Ithaca, New York, USA, 14–16 August 1996. ---- Introduction This document contains information relevant to the European ESPRIT Basic Research [http://idom-www.informatik.uni-hamburg.de/Esprit-BR/Synopses/Projects/8694.html ProCoS-WG Working Group] (no. 8694) of 24 academic and industrial partners interested in Provably Correct Systems associated with the ProCoS II project (no. 7071). A [http://vl.fmnet.info/procos/procos-wg/description.html ProCoS-WG description] of the objectives, activities, potential, etc., of the Working Group is available. A bibliography of relevant publications mainly by Working Group members has been produced in BibTeX format. A robot-based production cell has been chosen as a common case study for partners wishing to compare formal methods. As coordinators of the Working Group, the Oxford University Computing Laboratory welcomes visits by other Working Group sites and an online guide to Oxford is available. Synopsis ProCoS-WG — Provably Correct Systems Work Area Theories for Concurrency and Real-time; Specification and Verification COORDINATOR (Country) Oxford University (UK) Computing Laboratory Wolfson Building, Parks Road UK - OXFORD OX1 3QD Participants Graz University of Technology (A) DST Deutsche System Technik GmbH (D) Forschungszentrum Informatik, Karlsruhe (D) Universität Kiel (D) Universität Oldenburg (D) Philips GmbH Forschungslaboratorien (D) RWTÜV Anlagentechnik (D) Technische Hochschule Darmstadt (D) Danish State Railways (DK) IFAD (DK) Technical University of Denmark (DK) GEC Alsthom (F) Verimag (F) Politecnico di Milano (I) University of Oslo (N) University of Reading (UK) University of Twente (NL) Swedish Institute for Computer Science (S) &Aa;bo Akademi University (SF) University of Cambridge (UK) Lloyd's Register (UK) National Physical Laboratory (UK) Praxis Systems plc (UK) University of York (UK) CONTACT POINT Jonathan Bowen +44-118-931-6544 Fax: +44-118-975-1994 Email: [mailto:procos-request@comlab.ox.ac.uk procos-request@comlab.ox.ac.uk] Keywords: Programming Methodology, Safety-Critical Systems, Specification Languages, Programming Languages Start date: 1 January 94 Duration 36 months (extended by 6 months) Status: ended Abstract: The ProCoS-WG Working Group is based around the existing Basic Research project (7071) to aid dissemination of the project's results. ProCoS-WG aims to improve dependability, reduce timescales and cut development costs of construction for embedded systems, particularly in real-time and safety-critical applications. It uses and develops the results of basic research into fundamental properties of interactive systems. It aims to provide a scientific basis for future standards of practice in the development of embedded systems, ensuring correctness of all stages in the development, from elicitation and analysis of requirements through design and implementation of programs down to compilation and execution on verified hardware. ---- Aims ProCoS-WG aims to aid the dissemination of results of the existing project. The long term objective of the Working Group is to contribute to radical improvement in standards of professional practice in the design and implementation of information technology products, involving both hardware and software. The first target for improvement is in the area of safety critical application; but we believe that much of the same technology will eventually spin off to improve quality and reduce life cycle costs of other products in widespread use. Topics of interest to members of the Working Group include theories and methodology to handle the following: # Requirements capture and analysis; # System specification and design; # Programming language processing and compilation; # Machine hardware, including multiprogramming kernels; # Implementation in hardware down to gate level. ---- Activities The ProCoS-WG Working Group is closely associated with the [[ProCoS II|'ProCoS II' Basic Research project]] (7071). Joint workshops were held during the lifetime of that project, approximately every 6 months at project sites in Denmark, Germany and the UK. The 1st Working Group meeting was held at Gentoft, Denmark, 18-20 January 1994. An "active" photograph of the participants is available. The major event for the Working Group was an open School and Symposium organised jointly with the existing [ftp://ftp.comlab.ox.ac.uk/pub/Documents/procos/FTRTFT94-CFP2.ps.Z Formal Techniques in Real-Time and Fault-Tolerant Systems] series, held 19–23 September 1994 at Lübeck, Germany. A published proceedings is available as SpringerLNCS volume 863. ISBN 3-540-58468-4. The [http://vl.fmnet.info/procos/procos-wg/jan95.html 2nd ProCoS-WG meeting] (for ProCoS-WG participants and invited guests only) was held on 10-12 January 1995 in Oxford, UK, organized by Jonathan Bowen. Information for participants and an agenda including summaries of the talks and a copy of the original invitation are available. The [http://vl.fmnet.info/procos/procos-wg/aug95.html 3rd ProCoS-WG meeting] was held 21–23 August 1995 at the Hotel Marina, Vedb&ae;k, just outside Copenhagen, Denmark. The local organizers were Hans Rischel (programme) and Disa la Cour (secretary), ID/DTU. A theme of Linking Theories was suggested by Prof. Tony Hoare. The [http://vl.fmnet.info/procos/procos-wg/mar96.html 4th ProCoS-WG meeting], was held 11-13 March 1996, in Oldenburg, Germany, organized by Prof E-R. Olderog. An associated [http://vl.fmnet.info/procos/procos-us.html ProCoS-US] Hardware Synthesis and Verification Workshop was held at Cornell University, Ithaca, New York, USA, 14-16 August 1996. The last major meeting was the [http://vl.fmnet.info/procos/apr97/ 5th ProCoS-WG meeting], 7-9 April 1997, at the University of Reading, UK, in conjunction with ZUM'97 (see below). This was the 5th and final meeting of the Working Group. The local organizing secretary was Christina Simmons in the Department of Computer Science. The group also supports the Z User Meeting series of conferences. The 8th Z User Meeting (ZUM'94) was was held on 29–30 June 1994 at , , UK. The 9th International Conference of Z Users (ZUM'95) was held 7-9 September 1995 at the University of Limerick, Ireland, both supported by ProCoS-WG. The last meeting was ZUM'97 which was held at the University of , UK, 3–4 April 1997. ---- Potential The Working Group will seek a simplification of the technology produced by the [[ProCoS II|'ProCoS' project]] to make it truly useful for engineers in an industrial setting. We hope to be influential in the area of European and international standards, particularly for safety-critical systems. ---- Other information A 2-page formatted summary of the Working Group, on which the information above is based, and a more detailed 10-page article (published in [http://www.cs.unibo.it/~gorrieri/eatcs/bulletin Christina Simmons also provided some funded secretarial support. For further information please email [mailto:procos-request@comlab.ox.ac.uk procos-request@comlab.ox.ac.uk] and to join the postal and/or electronic mailing list, please send a request to [mailto:procos-list-request@comlab.ox.ac.uk procos-list-request@comlab.ox.ac.uk] (see some previous messages). At the OUCL, this list is gatewayed to the local Oxford University Computing Laboratory newsgroup [news:ox.comlab.procos ox.comlab.procos]. ---- See also * Research grant information. * Compiler verification by Paul Curzon including [http://www.cl.cam.ac.uk/users/pc/procos94.html The Verified Compilation of Vista Programs]. * Other ESPRIT Working Group synopses. ---- Maintained by Jonathan Bowen as part of the [[ProCoS|'ProCoS' archive]]. Category:Networks Category:ProCoS Category:1993